$\forall$$T$:Type, ${\it as}$,${\it cs}$,${\it bs}$,${\it ds}$:($T$ List).
\\[0ex]compat($T$; append(${\it as}$; ${\it bs}$); append(${\it cs}$; ${\it ds}$)) $\Rightarrow$ (${\it as}$ = ${\it cs}$) $\Rightarrow$ compat($T$; ${\it bs}$; ${\it ds}$)